(set-logic QF_UFLIA)
(set-info :source |
  These benchmarks were obtained from the KIND tool during verification of
  Lustre programs.  See also the lustre family of benchmarks in QF_LIA.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (<= 0 _n))
(declare-fun ___z2z___ (Int) Bool)
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z7z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Bool)
(declare-fun ___z9z___ (Int) Bool)
(declare-fun ___z10z___ (Int) Bool)
(declare-fun ___z11z___ (Int) Bool)
(declare-fun ___z12z___ (Int) Bool)
(declare-fun ___z13z___ (Int) Bool)
(declare-fun ___z14z___ (Int) Bool)
(declare-fun ___z15z___ (Int) Bool)
(declare-fun ___z19z___ (Int) Bool)
(declare-fun ___z20z___ (Int) Bool)
(declare-fun ___z21z___ (Int) Int)
(declare-fun ___z22z___ (Int) Bool)
(declare-fun ___z23z___ (Int) Bool)
(declare-fun ___z24z___ (Int) Int)
(declare-fun ___z25z___ (Int) Int)
(declare-fun ___z26z___ (Int) Int)
(declare-fun ___z33z___ (Int) Int)
(declare-fun ___z34z___ (Int) Int)
(declare-fun ___z35z___ (Int) Int)
(declare-fun ___z36z___ (Int) Bool)
(declare-fun ___z37z___ (Int) Int)
(declare-fun ___z38z___ (Int) Int)
(declare-fun ___z39z___ (Int) Bool)
(declare-fun ___z40z___ (Int) Bool)
(declare-fun ___z41z___ (Int) Int)
(declare-fun ___z42z___ (Int) Int)
(declare-fun ___z43z___ (Int) Int)
(declare-fun ___z44z___ (Int) Int)
(declare-fun ___z45z___ (Int) Bool)
(declare-fun ___z46z___ (Int) Bool)
(declare-fun ___z47z___ (Int) Int)
(declare-fun ___z48z___ (Int) Int)
(declare-fun ___z49z___ (Int) Int)
(declare-fun ___z50z___ (Int) Bool)
(declare-fun ___z51z___ (Int) Int)
(declare-fun ___z52z___ (Int) Int)
(declare-fun ___z53z___ (Int) Int)
(declare-fun ___z54z___ (Int) Bool)
(declare-fun ___z55z___ (Int) Int)
(declare-fun ___z56z___ (Int) Int)
(declare-fun ___z57z___ (Int) Int)
(declare-fun ___z58z___ (Int) Bool)
(declare-fun ___z59z___ (Int) Bool)
(declare-fun ___z60z___ (Int) Int)
(declare-fun ___z61z___ (Int) Int)
(declare-fun ___z62z___ (Int) Bool)
(declare-fun ___z63z___ (Int) Int)
(declare-fun ___z64z___ (Int) Bool)
(declare-fun ___z65z___ (Int) Int)
(declare-fun ___z66z___ (Int) Bool)
(declare-fun ___z67z___ (Int) Int)
(declare-fun ___z68z___ (Int) Int)
(declare-fun ___z69z___ (Int) Int)
(declare-fun ___z71z___ (Int) Int)
(declare-fun ___z72z___ (Int) Bool)
(declare-fun ___z73z___ (Int) Int)
(declare-fun ___z74z___ (Int) Int)
(declare-fun ___z75z___ (Int) Int)
(declare-fun ___z76z___ (Int) Int)
(declare-fun ___z77z___ (Int) Int)
(declare-fun ___z81z___ (Int) Int)
(push 1)
(assert (= (= _base 0) (___z72z___ 0)))
(assert (= (ite (= _base 0) 0 (___z76z___ (- 1))) (___z73z___ 0)))
(assert (= (ite (= _base 0) 0 (___z81z___ (- 1))) (___z74z___ 0)))
(assert (= (ite (= _base 0) 0 (___z77z___ (- 1))) (___z75z___ 0)))
(assert (= (ite (not (___z19z___ 0)) 0 1) (___z33z___ 0)))
(assert (let ((?v_0 (___z68z___ 0)) (?v_1 (___z55z___ 0))) (= (ite (___z72z___ 0) (___z71z___ 0) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ 0))) (ite (___z54z___ 0) (ite (not (= ?v_1 3)) 3 ?v_1) ?v_1) ?v_0)) (___z76z___ 0))))
(assert (= (ite (not (___z20z___ 0)) 0 1) (___z34z___ 0)))
(assert (let ((?v_0 (___z68z___ 0)) (?v_1 (___z48z___ 0))) (= (ite (___z72z___ 0) (___z75z___ 0) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ 0))) (ite (___z50z___ 0) (+ (- 1) ?v_1) ?v_1) (___z65z___ 0))) (___z77z___ 0))))
(assert (= (ite (not (___z14z___ 0)) 0 1) (___z35z___ 0)))
(assert (let ((?v_0 (= (___z68z___ 0) 2))) (= (and ?v_0 (and (<= (___z65z___ 0) 0) ?v_0)) (___z36z___ 0))))
(assert (let ((?v_0 (___z68z___ 0))) (= (ite (___z36z___ 0) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z37z___ 0))))
(assert (let ((?v_0 (___z68z___ 0)) (?v_1 (___z56z___ 0))) (= (ite (___z72z___ 0) (ite (not (= (___z73z___ 0) 4)) 1 (___z74z___ 0)) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ 0))) (ite (___z54z___ 0) (ite (not (= (___z55z___ 0) 3)) 3 ?v_1) ?v_1) (___z69z___ 0))) (___z81z___ 0))))
(assert (let ((?v_0 (___z37z___ 0))) (= (ite (___z36z___ 0) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z38z___ 0))))
(assert (= (and (and (not (___z36z___ 0)) (and (not (= (___z35z___ 0) 0)) (not (= (___z33z___ 0) 0)))) (= (___z38z___ 0) 3)) (___z39z___ 0)))
(assert (= (or (___z36z___ 0) (___z39z___ 0)) (___z40z___ 0)))
(assert (let ((?v_0 (___z38z___ 0))) (= (ite (___z39z___ 0) (ite (= ?v_0 3) 1 ?v_0) ?v_0) (___z41z___ 0))))
(assert (let ((?v_0 (___z69z___ 0))) (= (ite (___z36z___ 0) (ite (not (= (___z37z___ 0) 4)) 1 ?v_0) ?v_0) (___z42z___ 0))))
(assert (let ((?v_0 (___z41z___ 0))) (= (ite (___z39z___ 0) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z43z___ 0))))
(assert (let ((?v_0 (___z42z___ 0))) (= (ite (___z39z___ 0) (ite (not (= (___z41z___ 0) 2)) 2 ?v_0) ?v_0) (___z44z___ 0))))
(assert (let ((?v_1 (not (___z40z___ 0))) (?v_0 (= (___z43z___ 0) 3))) (= (and (and ?v_1 ?v_0) (and ?v_0 (and ?v_1 (not (= (___z34z___ 0) 0))))) (___z45z___ 0))))
(assert (= (or (___z40z___ 0) (___z45z___ 0)) (___z46z___ 0)))
(assert (let ((?v_0 (___z43z___ 0))) (= (ite (___z45z___ 0) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z47z___ 0))))
(assert (= (___z48z___ 0) (ite (___z45z___ 0) 0 (___z65z___ 0))))
(assert (let ((?v_0 (___z47z___ 0))) (= (ite (___z45z___ 0) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z49z___ 0))))
(assert (= (___z50z___ 0) (and (and (not (___z46z___ 0)) (not (<= (___z48z___ 0) 0))) (= (___z49z___ 0) 2))))
(assert (let ((?v_0 (___z44z___ 0))) (= (ite (___z45z___ 0) (ite (not (= (___z47z___ 0) 4)) 1 ?v_0) ?v_0) (___z51z___ 0))))
(assert (let ((?v_0 (___z49z___ 0))) (= (ite (___z50z___ 0) (ite (= ?v_0 2) 1 ?v_0) ?v_0) (___z52z___ 0))))
(assert (let ((?v_0 (___z52z___ 0))) (= (ite (___z50z___ 0) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z53z___ 0))))
(assert (= (___z54z___ 0) (and (and (not (or (___z50z___ 0) (___z46z___ 0))) (or (= (___z35z___ 0) 0) (not (= (___z34z___ 0) 0)))) (= (___z53z___ 0) 2))))
(assert (let ((?v_0 (___z53z___ 0))) (= (___z55z___ 0) (ite (___z54z___ 0) (ite (= ?v_0 2) 1 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z51z___ 0))) (= (___z56z___ 0) (ite (___z50z___ 0) (ite (not (= (___z52z___ 0) 2)) 2 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z67z___ 0))) (= (ite (not (and (<= ?v_0 3) (<= 1 ?v_0))) 1 ?v_0) (___z57z___ 0))))
(assert (let ((?v_0 (___z63z___ 0))) (= (or (= ?v_0 3) (= ?v_0 2)) (___z15z___ 0))))
(assert (let ((?v_1 (___z57z___ 0)) (?v_0 (___z67z___ 0))) (= (and (not (and (<= ?v_0 3) (<= 1 ?v_0))) (and (<= ?v_1 3) (<= 1 ?v_1))) (___z58z___ 0))))
(assert (let ((?v_0 (___z57z___ 0))) (= (and (___z58z___ 0) (and (not (= (___z35z___ 0) 0)) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z59z___ 0))))
(assert (let ((?v_0 (___z57z___ 0))) (= (ite (___z59z___ 0) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z60z___ 0))))
(assert (let ((?v_0 (___z74z___ 0))) (= (ite (___z59z___ 0) (ite (not (= (___z57z___ 0) 2)) 2 ?v_0) ?v_0) (___z61z___ 0))))
(assert (let ((?v_0 (= _base 0)) (?v_1 (___z2z___ 0))) (= (___z19z___ 0) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (not (___z2z___ (- 1)))))))))
(assert (let ((?v_0 (___z60z___ 0))) (= (and (___z58z___ 0) (and (not (___z59z___ 0)) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z62z___ 0))))
(assert (let ((?v_0 (= _base 0)) (?v_1 (___z3z___ 0))) (= (___z20z___ 0) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (not (___z3z___ (- 1)))))))))
(assert (let ((?v_0 (___z60z___ 0))) (= (___z63z___ 0) (ite (___z62z___ 0) (ite (not (= ?v_0 3)) 3 ?v_0) ?v_0))))
(assert (let ((?v_2 (+ (* 60 (___z24z___ 0)) (+ (* 10 (___z25z___ 0)) (___z26z___ 0)))) (?v_1 (___z22z___ 0))) (let ((?v_0 (and (not ?v_1) (___z23z___ 0)))) (= (ite (= _base 0) (ite ?v_0 0 ?v_2) (ite ?v_0 0 (ite ?v_1 ?v_2 (___z21z___ (- 1))))) (___z21z___ 0)))))
(assert (= (= (___z73z___ 0) 4) (___z64z___ 0)))
(assert (= (___z22z___ 0) (or (= _base 0) (= (___z81z___ (- 1)) 1))))
(assert (= (___z65z___ 0) (ite (___z64z___ 0) (___z21z___ 0) (___z75z___ 0))))
(assert (let ((?v_0 (___z22z___ (- 1)))) (= (___z23z___ 0) (or (= _base 0) (or (not (___z22z___ 0)) (and (not ?v_0) (or ?v_0 (___z23z___ (- 1)))))))))
(assert (= (___z66z___ 0) (and (___z64z___ 0) (and (= (___z73z___ 0) 4) (and (not (= (___z33z___ 0) 0)) (not (= (ite (<= (___z21z___ 0) 0) 0 1) 0)))))))
(assert (let ((?v_0 (___z24z___ (- 1)))) (= (___z24z___ 0) (ite (= _base 0) 0 (ite (___z22z___ 0) (ite (___z23z___ 0) 0 (ite (___z3z___ 0) 0 (ite (<= (ite (and (not (___z4z___ (- 1))) (___z4z___ 0)) 0 (ite (and (not (___z5z___ (- 1))) (___z5z___ 0)) 1 (ite (and (not (___z6z___ (- 1))) (___z6z___ 0)) 2 (ite (and (not (___z7z___ (- 1))) (___z7z___ 0)) 3 (ite (and (not (___z8z___ (- 1))) (___z8z___ 0)) 4 (ite (and (not (___z9z___ (- 1))) (___z9z___ 0)) 5 (ite (and (not (___z10z___ (- 1))) (___z10z___ 0)) 6 (ite (and (not (___z11z___ (- 1))) (___z11z___ 0)) 7 (ite (and (not (___z12z___ (- 1))) (___z12z___ 0)) 8 (ite (and (not (___z13z___ (- 1))) (___z13z___ 0)) 9 10)))))))))) 9) (___z25z___ (- 1)) ?v_0))) ?v_0)))))
(assert (let ((?v_0 (___z73z___ 0))) (= (___z67z___ 0) (ite (___z66z___ 0) (ite (= ?v_0 4) 0 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z25z___ (- 1)))) (= (___z25z___ 0) (ite (= _base 0) 0 (ite (___z22z___ 0) (ite (___z23z___ 0) 0 (ite (___z3z___ 0) 0 (ite (<= (ite (and (not (___z4z___ (- 1))) (___z4z___ 0)) 0 (ite (and (not (___z5z___ (- 1))) (___z5z___ 0)) 1 (ite (and (not (___z6z___ (- 1))) (___z6z___ 0)) 2 (ite (and (not (___z7z___ (- 1))) (___z7z___ 0)) 3 (ite (and (not (___z8z___ (- 1))) (___z8z___ 0)) 4 (ite (and (not (___z9z___ (- 1))) (___z9z___ 0)) 5 (ite (and (not (___z10z___ (- 1))) (___z10z___ 0)) 6 (ite (and (not (___z11z___ (- 1))) (___z11z___ 0)) 7 (ite (and (not (___z12z___ (- 1))) (___z12z___ 0)) 8 (ite (and (not (___z13z___ (- 1))) (___z13z___ 0)) 9 10)))))))))) 9) (___z26z___ (- 1)) ?v_0))) ?v_0)))))
(assert (= (___z68z___ 0) (ite (___z66z___ 0) (___z63z___ 0) (___z67z___ 0))))
(assert (let ((?v_2 (___z3z___ 0)) (?v_12 (___z13z___ 0)) (?v_11 (___z12z___ 0)) (?v_10 (___z11z___ 0)) (?v_9 (___z10z___ 0)) (?v_8 (___z9z___ 0)) (?v_7 (___z8z___ 0)) (?v_6 (___z7z___ 0)) (?v_5 (___z6z___ 0)) (?v_4 (___z5z___ 0)) (?v_3 (___z4z___ 0))) (let ((?v_0 (ite ?v_3 0 (ite ?v_4 1 (ite ?v_5 2 (ite ?v_6 3 (ite ?v_7 4 (ite ?v_8 5 (ite ?v_9 6 (ite ?v_10 7 (ite ?v_11 8 (ite ?v_12 9 10)))))))))))) (let ((?v_1 (ite ?v_2 0 (ite (<= ?v_0 9) ?v_0 0))) (?v_13 (ite (and (not (___z4z___ (- 1))) ?v_3) 0 (ite (and (not (___z5z___ (- 1))) ?v_4) 1 (ite (and (not (___z6z___ (- 1))) ?v_5) 2 (ite (and (not (___z7z___ (- 1))) ?v_6) 3 (ite (and (not (___z8z___ (- 1))) ?v_7) 4 (ite (and (not (___z9z___ (- 1))) ?v_8) 5 (ite (and (not (___z10z___ (- 1))) ?v_9) 6 (ite (and (not (___z11z___ (- 1))) ?v_10) 7 (ite (and (not (___z12z___ (- 1))) ?v_11) 8 (ite (and (not (___z13z___ (- 1))) ?v_12) 9 10))))))))))) (?v_14 (___z26z___ (- 1)))) (= (___z26z___ 0) (ite (= _base 0) ?v_1 (ite (___z22z___ 0) (ite (___z23z___ 0) ?v_1 (ite ?v_2 0 (ite (<= ?v_13 9) ?v_13 ?v_14))) ?v_14)))))))
(assert (let ((?v_0 (___z61z___ 0))) (= (___z69z___ 0) (ite (___z66z___ 0) (ite (___z62z___ 0) (ite (not (= (___z60z___ 0) 3)) 3 ?v_0) ?v_0) (___z74z___ 0)))))
(assert (let ((?v_0 (___z73z___ 0))) (= (___z71z___ 0) (ite (not (= ?v_0 4)) 4 ?v_0))))
(assert (= (= _base (- 1)) (___z72z___ (- 1))))
(assert (= (ite (= _base (- 1)) 0 (___z76z___ (- 2))) (___z73z___ (- 1))))
(assert (= (ite (= _base (- 1)) 0 (___z81z___ (- 2))) (___z74z___ (- 1))))
(assert (= (ite (= _base (- 1)) 0 (___z77z___ (- 2))) (___z75z___ (- 1))))
(assert (= (ite (not (___z19z___ (- 1))) 0 1) (___z33z___ (- 1))))
(assert (let ((?v_0 (___z68z___ (- 1))) (?v_1 (___z55z___ (- 1)))) (= (___z76z___ (- 1)) (ite (___z72z___ (- 1)) (___z71z___ (- 1)) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ (- 1)))) (ite (___z54z___ (- 1)) (ite (not (= ?v_1 3)) 3 ?v_1) ?v_1) ?v_0)))))
(assert (= (ite (not (___z20z___ (- 1))) 0 1) (___z34z___ (- 1))))
(assert (let ((?v_0 (___z68z___ (- 1))) (?v_1 (___z48z___ (- 1)))) (= (___z77z___ (- 1)) (ite (___z72z___ (- 1)) (___z75z___ (- 1)) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ (- 1)))) (ite (___z50z___ (- 1)) (+ (- 1) ?v_1) ?v_1) (___z65z___ (- 1)))))))
(assert (= (ite (not (___z14z___ (- 1))) 0 1) (___z35z___ (- 1))))
(assert (let ((?v_0 (= (___z68z___ (- 1)) 2))) (= (and ?v_0 (and (<= (___z65z___ (- 1)) 0) ?v_0)) (___z36z___ (- 1)))))
(assert (let ((?v_0 (___z68z___ (- 1)))) (= (ite (___z36z___ (- 1)) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z37z___ (- 1)))))
(assert (let ((?v_0 (___z68z___ (- 1))) (?v_1 (___z56z___ (- 1)))) (= (___z81z___ (- 1)) (ite (___z72z___ (- 1)) (ite (not (= (___z73z___ (- 1)) 4)) 1 (___z74z___ (- 1))) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ (- 1)))) (ite (___z54z___ (- 1)) (ite (not (= (___z55z___ (- 1)) 3)) 3 ?v_1) ?v_1) (___z69z___ (- 1)))))))
(assert (let ((?v_0 (___z37z___ (- 1)))) (= (ite (___z36z___ (- 1)) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z38z___ (- 1)))))
(assert (= (and (and (not (___z36z___ (- 1))) (and (not (= (___z35z___ (- 1)) 0)) (not (= (___z33z___ (- 1)) 0)))) (= (___z38z___ (- 1)) 3)) (___z39z___ (- 1))))
(assert (= (or (___z36z___ (- 1)) (___z39z___ (- 1))) (___z40z___ (- 1))))
(assert (let ((?v_0 (___z38z___ (- 1)))) (= (ite (___z39z___ (- 1)) (ite (= ?v_0 3) 1 ?v_0) ?v_0) (___z41z___ (- 1)))))
(assert (let ((?v_0 (___z69z___ (- 1)))) (= (ite (___z36z___ (- 1)) (ite (not (= (___z37z___ (- 1)) 4)) 1 ?v_0) ?v_0) (___z42z___ (- 1)))))
(assert (let ((?v_0 (___z41z___ (- 1)))) (= (ite (___z39z___ (- 1)) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z43z___ (- 1)))))
(assert (let ((?v_0 (___z42z___ (- 1)))) (= (ite (___z39z___ (- 1)) (ite (not (= (___z41z___ (- 1)) 2)) 2 ?v_0) ?v_0) (___z44z___ (- 1)))))
(assert (let ((?v_1 (not (___z40z___ (- 1)))) (?v_0 (= (___z43z___ (- 1)) 3))) (= (and (and ?v_1 ?v_0) (and ?v_0 (and ?v_1 (not (= (___z34z___ (- 1)) 0))))) (___z45z___ (- 1)))))
(assert (= (or (___z40z___ (- 1)) (___z45z___ (- 1))) (___z46z___ (- 1))))
(assert (let ((?v_0 (___z43z___ (- 1)))) (= (ite (___z45z___ (- 1)) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z47z___ (- 1)))))
(assert (= (___z48z___ (- 1)) (ite (___z45z___ (- 1)) 0 (___z65z___ (- 1)))))
(assert (let ((?v_0 (___z47z___ (- 1)))) (= (ite (___z45z___ (- 1)) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z49z___ (- 1)))))
(assert (= (___z50z___ (- 1)) (and (and (not (___z46z___ (- 1))) (not (<= (___z48z___ (- 1)) 0))) (= (___z49z___ (- 1)) 2))))
(assert (let ((?v_0 (___z44z___ (- 1)))) (= (ite (___z45z___ (- 1)) (ite (not (= (___z47z___ (- 1)) 4)) 1 ?v_0) ?v_0) (___z51z___ (- 1)))))
(assert (let ((?v_0 (___z49z___ (- 1)))) (= (ite (___z50z___ (- 1)) (ite (= ?v_0 2) 1 ?v_0) ?v_0) (___z52z___ (- 1)))))
(assert (let ((?v_0 (___z52z___ (- 1)))) (= (ite (___z50z___ (- 1)) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z53z___ (- 1)))))
(assert (= (___z54z___ (- 1)) (and (and (not (or (___z50z___ (- 1)) (___z46z___ (- 1)))) (or (= (___z35z___ (- 1)) 0) (not (= (___z34z___ (- 1)) 0)))) (= (___z53z___ (- 1)) 2))))
(assert (let ((?v_0 (___z53z___ (- 1)))) (= (___z55z___ (- 1)) (ite (___z54z___ (- 1)) (ite (= ?v_0 2) 1 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z51z___ (- 1)))) (= (___z56z___ (- 1)) (ite (___z50z___ (- 1)) (ite (not (= (___z52z___ (- 1)) 2)) 2 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z67z___ (- 1)))) (= (ite (not (and (<= ?v_0 3) (<= 1 ?v_0))) 1 ?v_0) (___z57z___ (- 1)))))
(assert (let ((?v_0 (___z63z___ (- 1)))) (= (or (= ?v_0 3) (= ?v_0 2)) (___z15z___ (- 1)))))
(assert (let ((?v_0 (___z67z___ (- 1))) (?v_1 (___z57z___ (- 1)))) (= (and (not (and (<= ?v_0 3) (<= 1 ?v_0))) (and (<= ?v_1 3) (<= 1 ?v_1))) (___z58z___ (- 1)))))
(assert (let ((?v_0 (___z57z___ (- 1)))) (= (and (___z58z___ (- 1)) (and (not (= (___z35z___ (- 1)) 0)) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z59z___ (- 1)))))
(assert (let ((?v_0 (___z57z___ (- 1)))) (= (ite (___z59z___ (- 1)) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z60z___ (- 1)))))
(assert (let ((?v_0 (___z74z___ (- 1)))) (= (ite (___z59z___ (- 1)) (ite (not (= (___z57z___ (- 1)) 2)) 2 ?v_0) ?v_0) (___z61z___ (- 1)))))
(assert (let ((?v_1 (___z2z___ (- 1))) (?v_0 (= _base (- 1)))) (= (___z19z___ (- 1)) (and (or ?v_1 (not ?v_0)) (or ?v_0 (and ?v_1 (not (___z2z___ (- 2)))))))))
(assert (let ((?v_0 (___z60z___ (- 1)))) (= (and (___z58z___ (- 1)) (and (not (___z59z___ (- 1))) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z62z___ (- 1)))))
(assert (let ((?v_1 (___z3z___ (- 1))) (?v_0 (= _base (- 1)))) (= (___z20z___ (- 1)) (and (or ?v_1 (not ?v_0)) (or ?v_0 (and ?v_1 (not (___z3z___ (- 2)))))))))
(assert (let ((?v_0 (___z60z___ (- 1)))) (= (___z63z___ (- 1)) (ite (___z62z___ (- 1)) (ite (not (= ?v_0 3)) 3 ?v_0) ?v_0))))
(assert (let ((?v_1 (___z22z___ (- 1)))) (let ((?v_0 (and (not ?v_1) (___z23z___ (- 1)))) (?v_2 (+ (* 60 (___z24z___ (- 1))) (+ (___z26z___ (- 1)) (* 10 (___z25z___ (- 1))))))) (= (___z21z___ (- 1)) (ite (= _base (- 1)) (ite ?v_0 0 ?v_2) (ite ?v_0 0 (ite ?v_1 ?v_2 (___z21z___ (- 2)))))))))
(assert (= (= (___z73z___ (- 1)) 4) (___z64z___ (- 1))))
(assert (= (___z22z___ (- 1)) (or (= _base (- 1)) (= (___z81z___ (- 2)) 1))))
(assert (= (___z65z___ (- 1)) (ite (___z64z___ (- 1)) (___z21z___ (- 1)) (___z75z___ (- 1)))))
(assert (let ((?v_0 (___z22z___ (- 2)))) (= (___z23z___ (- 1)) (or (= _base (- 1)) (or (not (___z22z___ (- 1))) (and (not ?v_0) (or ?v_0 (___z23z___ (- 2)))))))))
(assert (= (___z66z___ (- 1)) (and (___z64z___ (- 1)) (and (= (___z73z___ (- 1)) 4) (and (not (= (___z33z___ (- 1)) 0)) (not (= (ite (<= (___z21z___ (- 1)) 0) 0 1) 0)))))))
(assert (let ((?v_0 (___z24z___ (- 2)))) (= (___z24z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z22z___ (- 1)) (ite (___z23z___ (- 1)) 0 (ite (___z3z___ (- 1)) 0 (ite (<= (ite (and (___z4z___ (- 1)) (not (___z4z___ (- 2)))) 0 (ite (and (___z5z___ (- 1)) (not (___z5z___ (- 2)))) 1 (ite (and (___z6z___ (- 1)) (not (___z6z___ (- 2)))) 2 (ite (and (___z7z___ (- 1)) (not (___z7z___ (- 2)))) 3 (ite (and (___z8z___ (- 1)) (not (___z8z___ (- 2)))) 4 (ite (and (___z9z___ (- 1)) (not (___z9z___ (- 2)))) 5 (ite (and (___z10z___ (- 1)) (not (___z10z___ (- 2)))) 6 (ite (and (___z11z___ (- 1)) (not (___z11z___ (- 2)))) 7 (ite (and (___z12z___ (- 1)) (not (___z12z___ (- 2)))) 8 (ite (and (___z13z___ (- 1)) (not (___z13z___ (- 2)))) 9 10)))))))))) 9) (___z25z___ (- 2)) ?v_0))) ?v_0)))))
(assert (let ((?v_0 (___z73z___ (- 1)))) (= (___z67z___ (- 1)) (ite (___z66z___ (- 1)) (ite (= ?v_0 4) 0 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z25z___ (- 2)))) (= (___z25z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z22z___ (- 1)) (ite (___z23z___ (- 1)) 0 (ite (___z3z___ (- 1)) 0 (ite (<= (ite (and (___z4z___ (- 1)) (not (___z4z___ (- 2)))) 0 (ite (and (___z5z___ (- 1)) (not (___z5z___ (- 2)))) 1 (ite (and (___z6z___ (- 1)) (not (___z6z___ (- 2)))) 2 (ite (and (___z7z___ (- 1)) (not (___z7z___ (- 2)))) 3 (ite (and (___z8z___ (- 1)) (not (___z8z___ (- 2)))) 4 (ite (and (___z9z___ (- 1)) (not (___z9z___ (- 2)))) 5 (ite (and (___z10z___ (- 1)) (not (___z10z___ (- 2)))) 6 (ite (and (___z11z___ (- 1)) (not (___z11z___ (- 2)))) 7 (ite (and (___z12z___ (- 1)) (not (___z12z___ (- 2)))) 8 (ite (and (___z13z___ (- 1)) (not (___z13z___ (- 2)))) 9 10)))))))))) 9) (___z26z___ (- 2)) ?v_0))) ?v_0)))))
(assert (= (___z68z___ (- 1)) (ite (___z66z___ (- 1)) (___z63z___ (- 1)) (___z67z___ (- 1)))))
(assert (let ((?v_2 (___z3z___ (- 1))) (?v_3 (___z4z___ (- 1))) (?v_4 (___z5z___ (- 1))) (?v_5 (___z6z___ (- 1))) (?v_6 (___z7z___ (- 1))) (?v_7 (___z8z___ (- 1))) (?v_8 (___z9z___ (- 1))) (?v_9 (___z10z___ (- 1))) (?v_10 (___z11z___ (- 1))) (?v_11 (___z12z___ (- 1))) (?v_12 (___z13z___ (- 1)))) (let ((?v_13 (ite (and ?v_3 (not (___z4z___ (- 2)))) 0 (ite (and ?v_4 (not (___z5z___ (- 2)))) 1 (ite (and ?v_5 (not (___z6z___ (- 2)))) 2 (ite (and ?v_6 (not (___z7z___ (- 2)))) 3 (ite (and ?v_7 (not (___z8z___ (- 2)))) 4 (ite (and ?v_8 (not (___z9z___ (- 2)))) 5 (ite (and ?v_9 (not (___z10z___ (- 2)))) 6 (ite (and ?v_10 (not (___z11z___ (- 2)))) 7 (ite (and ?v_11 (not (___z12z___ (- 2)))) 8 (ite (and ?v_12 (not (___z13z___ (- 2)))) 9 10))))))))))) (?v_14 (___z26z___ (- 2))) (?v_0 (ite ?v_3 0 (ite ?v_4 1 (ite ?v_5 2 (ite ?v_6 3 (ite ?v_7 4 (ite ?v_8 5 (ite ?v_9 6 (ite ?v_10 7 (ite ?v_11 8 (ite ?v_12 9 10)))))))))))) (let ((?v_1 (ite ?v_2 0 (ite (<= ?v_0 9) ?v_0 0)))) (= (___z26z___ (- 1)) (ite (= _base (- 1)) ?v_1 (ite (___z22z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 (ite ?v_2 0 (ite (<= ?v_13 9) ?v_13 ?v_14))) ?v_14)))))))
(assert (let ((?v_0 (___z61z___ (- 1)))) (= (___z69z___ (- 1)) (ite (___z66z___ (- 1)) (ite (___z62z___ (- 1)) (ite (not (= (___z60z___ (- 1)) 3)) 3 ?v_0) ?v_0) (___z74z___ (- 1))))))
(assert (let ((?v_0 (___z73z___ (- 1)))) (= (___z71z___ (- 1)) (ite (not (= ?v_0 4)) 4 ?v_0))))
(push 1)
(assert (not (or (not (= _base (- 1))) (and (___z15z___ 0) (___z15z___ (- 1))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z15z___ (- 1)))
(assert (___z15z___ (- 2)))
(push 1)
(assert (= (= _n _base) (___z72z___ _n)))
(assert (= (ite (= _n _base) 0 (___z76z___ (+ _n (- 1)))) (___z73z___ _n)))
(assert (= (ite (= _n _base) 0 (___z81z___ (+ _n (- 1)))) (___z74z___ _n)))
(assert (= (ite (= _n _base) 0 (___z77z___ (+ _n (- 1)))) (___z75z___ _n)))
(assert (= (ite (not (___z19z___ _n)) 0 1) (___z33z___ _n)))
(assert (let ((?v_0 (___z68z___ _n)) (?v_1 (___z55z___ _n))) (= (ite (___z72z___ _n) (___z71z___ _n) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ _n))) (ite (___z54z___ _n) (ite (not (= ?v_1 3)) 3 ?v_1) ?v_1) ?v_0)) (___z76z___ _n))))
(assert (= (ite (not (___z20z___ _n)) 0 1) (___z34z___ _n)))
(assert (let ((?v_0 (___z68z___ _n)) (?v_1 (___z48z___ _n))) (= (ite (___z72z___ _n) (___z75z___ _n) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ _n))) (ite (___z50z___ _n) (+ (- 1) ?v_1) ?v_1) (___z65z___ _n))) (___z77z___ _n))))
(assert (= (ite (not (___z14z___ _n)) 0 1) (___z35z___ _n)))
(assert (let ((?v_0 (= (___z68z___ _n) 2))) (= (and ?v_0 (and (<= (___z65z___ _n) 0) ?v_0)) (___z36z___ _n))))
(assert (let ((?v_0 (___z68z___ _n))) (= (ite (___z36z___ _n) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z37z___ _n))))
(assert (let ((?v_0 (___z68z___ _n)) (?v_1 (___z56z___ _n))) (= (ite (___z72z___ _n) (ite (not (= (___z73z___ _n) 4)) 1 (___z74z___ _n)) (ite (and (and (<= ?v_0 3) (<= 1 ?v_0)) (not (___z66z___ _n))) (ite (___z54z___ _n) (ite (not (= (___z55z___ _n) 3)) 3 ?v_1) ?v_1) (___z69z___ _n))) (___z81z___ _n))))
(assert (let ((?v_0 (___z37z___ _n))) (= (ite (___z36z___ _n) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z38z___ _n))))
(assert (= (and (and (not (___z36z___ _n)) (and (not (= (___z35z___ _n) 0)) (not (= (___z33z___ _n) 0)))) (= (___z38z___ _n) 3)) (___z39z___ _n)))
(assert (= (or (___z36z___ _n) (___z39z___ _n)) (___z40z___ _n)))
(assert (let ((?v_0 (___z38z___ _n))) (= (ite (___z39z___ _n) (ite (= ?v_0 3) 1 ?v_0) ?v_0) (___z41z___ _n))))
(assert (let ((?v_0 (___z69z___ _n))) (= (ite (___z36z___ _n) (ite (not (= (___z37z___ _n) 4)) 1 ?v_0) ?v_0) (___z42z___ _n))))
(assert (let ((?v_0 (___z41z___ _n))) (= (ite (___z39z___ _n) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z43z___ _n))))
(assert (let ((?v_0 (___z42z___ _n))) (= (ite (___z39z___ _n) (ite (not (= (___z41z___ _n) 2)) 2 ?v_0) ?v_0) (___z44z___ _n))))
(assert (let ((?v_1 (not (___z40z___ _n))) (?v_0 (= (___z43z___ _n) 3))) (= (and (and ?v_1 ?v_0) (and ?v_0 (and ?v_1 (not (= (___z34z___ _n) 0))))) (___z45z___ _n))))
(assert (= (or (___z40z___ _n) (___z45z___ _n)) (___z46z___ _n)))
(assert (let ((?v_0 (___z43z___ _n))) (= (ite (___z45z___ _n) (ite (and (<= ?v_0 3) (<= 1 ?v_0)) 0 ?v_0) ?v_0) (___z47z___ _n))))
(assert (= (___z48z___ _n) (ite (___z45z___ _n) 0 (___z65z___ _n))))
(assert (let ((?v_0 (___z47z___ _n))) (= (ite (___z45z___ _n) (ite (not (= ?v_0 4)) 4 ?v_0) ?v_0) (___z49z___ _n))))
(assert (= (___z50z___ _n) (and (and (not (___z46z___ _n)) (not (<= (___z48z___ _n) 0))) (= (___z49z___ _n) 2))))
(assert (let ((?v_0 (___z44z___ _n))) (= (ite (___z45z___ _n) (ite (not (= (___z47z___ _n) 4)) 1 ?v_0) ?v_0) (___z51z___ _n))))
(assert (let ((?v_0 (___z49z___ _n))) (= (ite (___z50z___ _n) (ite (= ?v_0 2) 1 ?v_0) ?v_0) (___z52z___ _n))))
(assert (let ((?v_0 (___z52z___ _n))) (= (ite (___z50z___ _n) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z53z___ _n))))
(assert (= (___z54z___ _n) (and (and (not (or (___z50z___ _n) (___z46z___ _n))) (or (= (___z35z___ _n) 0) (not (= (___z34z___ _n) 0)))) (= (___z53z___ _n) 2))))
(assert (let ((?v_0 (___z53z___ _n))) (= (___z55z___ _n) (ite (___z54z___ _n) (ite (= ?v_0 2) 1 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z51z___ _n))) (= (___z56z___ _n) (ite (___z50z___ _n) (ite (not (= (___z52z___ _n) 2)) 2 ?v_0) ?v_0))))
(assert (let ((?v_0 (___z67z___ _n))) (= (ite (not (and (<= ?v_0 3) (<= 1 ?v_0))) 1 ?v_0) (___z57z___ _n))))
(assert (let ((?v_0 (___z63z___ _n))) (= (or (= ?v_0 3) (= ?v_0 2)) (___z15z___ _n))))
(assert (let ((?v_1 (___z57z___ _n)) (?v_0 (___z67z___ _n))) (= (and (not (and (<= ?v_0 3) (<= 1 ?v_0))) (and (<= ?v_1 3) (<= 1 ?v_1))) (___z58z___ _n))))
(assert (let ((?v_0 (___z57z___ _n))) (= (and (___z58z___ _n) (and (not (= (___z35z___ _n) 0)) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z59z___ _n))))
(assert (let ((?v_0 (___z57z___ _n))) (= (ite (___z59z___ _n) (ite (not (= ?v_0 2)) 2 ?v_0) ?v_0) (___z60z___ _n))))
(assert (let ((?v_0 (___z74z___ _n))) (= (ite (___z59z___ _n) (ite (not (= (___z57z___ _n) 2)) 2 ?v_0) ?v_0) (___z61z___ _n))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (___z2z___ _n))) (= (___z19z___ _n) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (not (___z2z___ (+ _n (- 1))))))))))
(assert (let ((?v_0 (___z60z___ _n))) (= (and (___z58z___ _n) (and (not (___z59z___ _n)) (and (<= ?v_0 3) (<= 1 ?v_0)))) (___z62z___ _n))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (___z3z___ _n))) (= (___z20z___ _n) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (not (___z3z___ (+ _n (- 1))))))))))
(assert (let ((?v_0 (___z60z___ _n))) (= (___z63z___ _n) (ite (___z62z___ _n) (ite (not (= ?v_0 3)) 3 ?v_0) ?v_0))))
(assert (let ((?v_2 (+ (* 60 (___z24z___ _n)) (+ (* 10 (___z25z___ _n)) (___z26z___ _n)))) (?v_1 (___z22z___ _n))) (let ((?v_0 (and (not ?v_1) (___z23z___ _n)))) (= (ite (= _n _base) (ite ?v_0 0 ?v_2) (ite ?v_0 0 (ite ?v_1 ?v_2 (___z21z___ (+ _n (- 1)))))) (___z21z___ _n)))))
(assert (= (= (___z73z___ _n) 4) (___z64z___ _n)))
(assert (= (___z22z___ _n) (or (= _n _base) (= (___z81z___ (+ _n (- 1))) 1))))
(assert (= (___z65z___ _n) (ite (___z64z___ _n) (___z21z___ _n) (___z75z___ _n))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_0 (___z22z___ ?v_1))) (= (___z23z___ _n) (or (= _n _base) (or (not (___z22z___ _n)) (and (not ?v_0) (or ?v_0 (___z23z___ ?v_1)))))))))
(assert (= (___z66z___ _n) (and (___z64z___ _n) (and (= (___z73z___ _n) 4) (and (not (= (___z33z___ _n) 0)) (not (= (ite (<= (___z21z___ _n) 0) 0 1) 0)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z24z___ ?v_0))) (= (___z24z___ _n) (ite (= _n _base) 0 (ite (___z22z___ _n) (ite (___z23z___ _n) 0 (ite (___z3z___ _n) 0 (ite (<= (ite (and (not (___z4z___ ?v_0)) (___z4z___ _n)) 0 (ite (and (not (___z5z___ ?v_0)) (___z5z___ _n)) 1 (ite (and (not (___z6z___ ?v_0)) (___z6z___ _n)) 2 (ite (and (not (___z7z___ ?v_0)) (___z7z___ _n)) 3 (ite (and (not (___z8z___ ?v_0)) (___z8z___ _n)) 4 (ite (and (not (___z9z___ ?v_0)) (___z9z___ _n)) 5 (ite (and (not (___z10z___ ?v_0)) (___z10z___ _n)) 6 (ite (and (not (___z11z___ ?v_0)) (___z11z___ _n)) 7 (ite (and (not (___z12z___ ?v_0)) (___z12z___ _n)) 8 (ite (and (not (___z13z___ ?v_0)) (___z13z___ _n)) 9 10)))))))))) 9) (___z25z___ ?v_0) ?v_1))) ?v_1))))))
(assert (let ((?v_0 (___z73z___ _n))) (= (___z67z___ _n) (ite (___z66z___ _n) (ite (= ?v_0 4) 0 ?v_0) ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z25z___ ?v_0))) (= (___z25z___ _n) (ite (= _n _base) 0 (ite (___z22z___ _n) (ite (___z23z___ _n) 0 (ite (___z3z___ _n) 0 (ite (<= (ite (and (not (___z4z___ ?v_0)) (___z4z___ _n)) 0 (ite (and (not (___z5z___ ?v_0)) (___z5z___ _n)) 1 (ite (and (not (___z6z___ ?v_0)) (___z6z___ _n)) 2 (ite (and (not (___z7z___ ?v_0)) (___z7z___ _n)) 3 (ite (and (not (___z8z___ ?v_0)) (___z8z___ _n)) 4 (ite (and (not (___z9z___ ?v_0)) (___z9z___ _n)) 5 (ite (and (not (___z10z___ ?v_0)) (___z10z___ _n)) 6 (ite (and (not (___z11z___ ?v_0)) (___z11z___ _n)) 7 (ite (and (not (___z12z___ ?v_0)) (___z12z___ _n)) 8 (ite (and (not (___z13z___ ?v_0)) (___z13z___ _n)) 9 10)))))))))) 9) (___z26z___ ?v_0) ?v_1))) ?v_1))))))
(assert (= (___z68z___ _n) (ite (___z66z___ _n) (___z63z___ _n) (___z67z___ _n))))
(assert (let ((?v_2 (___z3z___ _n)) (?v_13 (___z13z___ _n)) (?v_12 (___z12z___ _n)) (?v_11 (___z11z___ _n)) (?v_10 (___z10z___ _n)) (?v_9 (___z9z___ _n)) (?v_8 (___z8z___ _n)) (?v_7 (___z7z___ _n)) (?v_6 (___z6z___ _n)) (?v_5 (___z5z___ _n)) (?v_3 (___z4z___ _n))) (let ((?v_0 (ite ?v_3 0 (ite ?v_5 1 (ite ?v_6 2 (ite ?v_7 3 (ite ?v_8 4 (ite ?v_9 5 (ite ?v_10 6 (ite ?v_11 7 (ite ?v_12 8 (ite ?v_13 9 10)))))))))))) (let ((?v_1 (ite ?v_2 0 (ite (<= ?v_0 9) ?v_0 0))) (?v_4 (+ _n (- 1)))) (let ((?v_14 (ite (and (not (___z4z___ ?v_4)) ?v_3) 0 (ite (and (not (___z5z___ ?v_4)) ?v_5) 1 (ite (and (not (___z6z___ ?v_4)) ?v_6) 2 (ite (and (not (___z7z___ ?v_4)) ?v_7) 3 (ite (and (not (___z8z___ ?v_4)) ?v_8) 4 (ite (and (not (___z9z___ ?v_4)) ?v_9) 5 (ite (and (not (___z10z___ ?v_4)) ?v_10) 6 (ite (and (not (___z11z___ ?v_4)) ?v_11) 7 (ite (and (not (___z12z___ ?v_4)) ?v_12) 8 (ite (and (not (___z13z___ ?v_4)) ?v_13) 9 10))))))))))) (?v_15 (___z26z___ ?v_4))) (= (___z26z___ _n) (ite (= _n _base) ?v_1 (ite (___z22z___ _n) (ite (___z23z___ _n) ?v_1 (ite ?v_2 0 (ite (<= ?v_14 9) ?v_14 ?v_15))) ?v_15))))))))
(assert (let ((?v_0 (___z61z___ _n))) (= (___z69z___ _n) (ite (___z66z___ _n) (ite (___z62z___ _n) (ite (not (= (___z60z___ _n) 3)) 3 ?v_0) ?v_0) (___z74z___ _n)))))
(assert (let ((?v_0 (___z73z___ _n))) (= (___z71z___ _n) (ite (not (= ?v_0 4)) 4 ?v_0))))
(assert (= (= (+ _n (* (- 1) _base)) 1) (___z72z___ (+ _n (- 1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (= (+ _n (* (- 1) _base)) 1) 0 (___z76z___ (+ (- 1) ?v_0))) (___z73z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (= (+ _n (* (- 1) _base)) 1) 0 (___z81z___ (+ (- 1) ?v_0))) (___z74z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (= (+ _n (* (- 1) _base)) 1) 0 (___z77z___ (+ (- 1) ?v_0))) (___z75z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (not (___z19z___ ?v_0)) 0 1) (___z33z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z68z___ ?v_0)) (?v_2 (___z55z___ ?v_0))) (= (___z76z___ ?v_0) (ite (___z72z___ ?v_0) (___z71z___ ?v_0) (ite (and (and (<= ?v_1 3) (<= 1 ?v_1)) (not (___z66z___ ?v_0))) (ite (___z54z___ ?v_0) (ite (not (= ?v_2 3)) 3 ?v_2) ?v_2) ?v_1))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (not (___z20z___ ?v_0)) 0 1) (___z34z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z68z___ ?v_0)) (?v_2 (___z48z___ ?v_0))) (= (___z77z___ ?v_0) (ite (___z72z___ ?v_0) (___z75z___ ?v_0) (ite (and (and (<= ?v_1 3) (<= 1 ?v_1)) (not (___z66z___ ?v_0))) (ite (___z50z___ ?v_0) (+ (- 1) ?v_2) ?v_2) (___z65z___ ?v_0)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (ite (not (___z14z___ ?v_0)) 0 1) (___z35z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (= (___z68z___ ?v_0) 2))) (= (and ?v_1 (and (<= (___z65z___ ?v_0) 0) ?v_1)) (___z36z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z68z___ ?v_0))) (= (ite (___z36z___ ?v_0) (ite (and (<= ?v_1 3) (<= 1 ?v_1)) 0 ?v_1) ?v_1) (___z37z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z68z___ ?v_0)) (?v_2 (___z56z___ ?v_0))) (= (___z81z___ ?v_0) (ite (___z72z___ ?v_0) (ite (not (= (___z73z___ ?v_0) 4)) 1 (___z74z___ ?v_0)) (ite (and (and (<= ?v_1 3) (<= 1 ?v_1)) (not (___z66z___ ?v_0))) (ite (___z54z___ ?v_0) (ite (not (= (___z55z___ ?v_0) 3)) 3 ?v_2) ?v_2) (___z69z___ ?v_0)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z37z___ ?v_0))) (= (ite (___z36z___ ?v_0) (ite (not (= ?v_1 4)) 4 ?v_1) ?v_1) (___z38z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (and (and (not (___z36z___ ?v_0)) (and (not (= (___z35z___ ?v_0) 0)) (not (= (___z33z___ ?v_0) 0)))) (= (___z38z___ ?v_0) 3)) (___z39z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (or (___z36z___ ?v_0) (___z39z___ ?v_0)) (___z40z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z38z___ ?v_0))) (= (ite (___z39z___ ?v_0) (ite (= ?v_1 3) 1 ?v_1) ?v_1) (___z41z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z69z___ ?v_0))) (= (ite (___z36z___ ?v_0) (ite (not (= (___z37z___ ?v_0) 4)) 1 ?v_1) ?v_1) (___z42z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z41z___ ?v_0))) (= (ite (___z39z___ ?v_0) (ite (not (= ?v_1 2)) 2 ?v_1) ?v_1) (___z43z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z42z___ ?v_0))) (= (ite (___z39z___ ?v_0) (ite (not (= (___z41z___ ?v_0) 2)) 2 ?v_1) ?v_1) (___z44z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (not (___z40z___ ?v_0))) (?v_1 (= (___z43z___ ?v_0) 3))) (= (and (and ?v_2 ?v_1) (and ?v_1 (and ?v_2 (not (= (___z34z___ ?v_0) 0))))) (___z45z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (or (___z40z___ ?v_0) (___z45z___ ?v_0)) (___z46z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z43z___ ?v_0))) (= (ite (___z45z___ ?v_0) (ite (and (<= ?v_1 3) (<= 1 ?v_1)) 0 ?v_1) ?v_1) (___z47z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z48z___ ?v_0) (ite (___z45z___ ?v_0) 0 (___z65z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z47z___ ?v_0))) (= (ite (___z45z___ ?v_0) (ite (not (= ?v_1 4)) 4 ?v_1) ?v_1) (___z49z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z50z___ ?v_0) (and (and (not (___z46z___ ?v_0)) (not (<= (___z48z___ ?v_0) 0))) (= (___z49z___ ?v_0) 2)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z44z___ ?v_0))) (= (ite (___z45z___ ?v_0) (ite (not (= (___z47z___ ?v_0) 4)) 1 ?v_1) ?v_1) (___z51z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z49z___ ?v_0))) (= (ite (___z50z___ ?v_0) (ite (= ?v_1 2) 1 ?v_1) ?v_1) (___z52z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z52z___ ?v_0))) (= (ite (___z50z___ ?v_0) (ite (not (= ?v_1 2)) 2 ?v_1) ?v_1) (___z53z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z54z___ ?v_0) (and (and (not (or (___z50z___ ?v_0) (___z46z___ ?v_0))) (or (= (___z35z___ ?v_0) 0) (not (= (___z34z___ ?v_0) 0)))) (= (___z53z___ ?v_0) 2)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z53z___ ?v_0))) (= (___z55z___ ?v_0) (ite (___z54z___ ?v_0) (ite (= ?v_1 2) 1 ?v_1) ?v_1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z51z___ ?v_0))) (= (___z56z___ ?v_0) (ite (___z50z___ ?v_0) (ite (not (= (___z52z___ ?v_0) 2)) 2 ?v_1) ?v_1)))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_0 (___z67z___ ?v_1))) (= (ite (not (and (<= ?v_0 3) (<= 1 ?v_0))) 1 ?v_0) (___z57z___ ?v_1)))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_0 (___z63z___ ?v_1))) (= (or (= ?v_0 3) (= ?v_0 2)) (___z15z___ ?v_1)))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_0 (___z67z___ ?v_1)) (?v_2 (___z57z___ ?v_1))) (= (and (not (and (<= ?v_0 3) (<= 1 ?v_0))) (and (<= ?v_2 3) (<= 1 ?v_2))) (___z58z___ ?v_1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z57z___ ?v_0))) (= (and (___z58z___ ?v_0) (and (not (= (___z35z___ ?v_0) 0)) (and (<= ?v_1 3) (<= 1 ?v_1)))) (___z59z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z57z___ ?v_0))) (= (ite (___z59z___ ?v_0) (ite (not (= ?v_1 2)) 2 ?v_1) ?v_1) (___z60z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z74z___ ?v_0))) (= (ite (___z59z___ ?v_0) (ite (not (= (___z57z___ ?v_0) 2)) 2 ?v_1) ?v_1) (___z61z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (___z2z___ ?v_0)) (?v_1 (= (+ _n (* (- 1) _base)) 1))) (= (___z19z___ ?v_0) (and (or ?v_2 (not ?v_1)) (or ?v_1 (and ?v_2 (not (___z2z___ (+ (- 1) ?v_0))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z60z___ ?v_0))) (= (and (___z58z___ ?v_0) (and (not (___z59z___ ?v_0)) (and (<= ?v_1 3) (<= 1 ?v_1)))) (___z62z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (___z3z___ ?v_0)) (?v_1 (= (+ _n (* (- 1) _base)) 1))) (= (___z20z___ ?v_0) (and (or ?v_2 (not ?v_1)) (or ?v_1 (and ?v_2 (not (___z3z___ (+ (- 1) ?v_0))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z60z___ ?v_0))) (= (___z63z___ ?v_0) (ite (___z62z___ ?v_0) (ite (not (= ?v_1 3)) 3 ?v_1) ?v_1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (___z22z___ ?v_0))) (let ((?v_1 (and (not ?v_2) (___z23z___ ?v_0))) (?v_3 (+ (* 60 (___z24z___ ?v_0)) (+ (___z26z___ ?v_0) (* 10 (___z25z___ ?v_0)))))) (= (___z21z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) (ite ?v_1 0 ?v_3) (ite ?v_1 0 (ite ?v_2 ?v_3 (___z21z___ (+ (- 1) ?v_0))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z73z___ ?v_0) 4) (___z64z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z22z___ ?v_0) (or (= (+ _n (* (- 1) _base)) 1) (= (___z81z___ (+ (- 1) ?v_0)) 1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z65z___ ?v_0) (ite (___z64z___ ?v_0) (___z21z___ ?v_0) (___z75z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (+ (- 1) ?v_0))) (let ((?v_1 (___z22z___ ?v_2))) (= (___z23z___ ?v_0) (or (= (+ _n (* (- 1) _base)) 1) (or (not (___z22z___ ?v_0)) (and (not ?v_1) (or ?v_1 (___z23z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z66z___ ?v_0) (and (___z64z___ ?v_0) (and (= (___z73z___ ?v_0) 4) (and (not (= (___z33z___ ?v_0) 0)) (not (= (ite (<= (___z21z___ ?v_0) 0) 0 1) 0))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (let ((?v_2 (___z24z___ ?v_1))) (= (___z24z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (___z22z___ ?v_0) (ite (___z23z___ ?v_0) 0 (ite (___z3z___ ?v_0) 0 (ite (<= (ite (and (___z4z___ ?v_0) (not (___z4z___ ?v_1))) 0 (ite (and (___z5z___ ?v_0) (not (___z5z___ ?v_1))) 1 (ite (and (___z6z___ ?v_0) (not (___z6z___ ?v_1))) 2 (ite (and (___z7z___ ?v_0) (not (___z7z___ ?v_1))) 3 (ite (and (___z8z___ ?v_0) (not (___z8z___ ?v_1))) 4 (ite (and (___z9z___ ?v_0) (not (___z9z___ ?v_1))) 5 (ite (and (___z10z___ ?v_0) (not (___z10z___ ?v_1))) 6 (ite (and (___z11z___ ?v_0) (not (___z11z___ ?v_1))) 7 (ite (and (___z12z___ ?v_0) (not (___z12z___ ?v_1))) 8 (ite (and (___z13z___ ?v_0) (not (___z13z___ ?v_1))) 9 10)))))))))) 9) (___z25z___ ?v_1) ?v_2))) ?v_2)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z73z___ ?v_0))) (= (___z67z___ ?v_0) (ite (___z66z___ ?v_0) (ite (= ?v_1 4) 0 ?v_1) ?v_1)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (let ((?v_2 (___z25z___ ?v_1))) (= (___z25z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (___z22z___ ?v_0) (ite (___z23z___ ?v_0) 0 (ite (___z3z___ ?v_0) 0 (ite (<= (ite (and (___z4z___ ?v_0) (not (___z4z___ ?v_1))) 0 (ite (and (___z5z___ ?v_0) (not (___z5z___ ?v_1))) 1 (ite (and (___z6z___ ?v_0) (not (___z6z___ ?v_1))) 2 (ite (and (___z7z___ ?v_0) (not (___z7z___ ?v_1))) 3 (ite (and (___z8z___ ?v_0) (not (___z8z___ ?v_1))) 4 (ite (and (___z9z___ ?v_0) (not (___z9z___ ?v_1))) 5 (ite (and (___z10z___ ?v_0) (not (___z10z___ ?v_1))) 6 (ite (and (___z11z___ ?v_0) (not (___z11z___ ?v_1))) 7 (ite (and (___z12z___ ?v_0) (not (___z12z___ ?v_1))) 8 (ite (and (___z13z___ ?v_0) (not (___z13z___ ?v_1))) 9 10)))))))))) 9) (___z26z___ ?v_1) ?v_2))) ?v_2)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z68z___ ?v_0) (ite (___z66z___ ?v_0) (___z63z___ ?v_0) (___z67z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_3 (___z3z___ ?v_0)) (?v_4 (___z4z___ ?v_0)) (?v_5 (___z5z___ ?v_0)) (?v_7 (___z6z___ ?v_0)) (?v_8 (___z7z___ ?v_0)) (?v_9 (___z8z___ ?v_0)) (?v_10 (___z9z___ ?v_0)) (?v_11 (___z10z___ ?v_0)) (?v_12 (___z11z___ ?v_0)) (?v_13 (___z12z___ ?v_0)) (?v_14 (___z13z___ ?v_0)) (?v_6 (+ (- 1) ?v_0))) (let ((?v_15 (ite (and ?v_4 (not (___z4z___ ?v_6))) 0 (ite (and ?v_5 (not (___z5z___ ?v_6))) 1 (ite (and ?v_7 (not (___z6z___ ?v_6))) 2 (ite (and ?v_8 (not (___z7z___ ?v_6))) 3 (ite (and ?v_9 (not (___z8z___ ?v_6))) 4 (ite (and ?v_10 (not (___z9z___ ?v_6))) 5 (ite (and ?v_11 (not (___z10z___ ?v_6))) 6 (ite (and ?v_12 (not (___z11z___ ?v_6))) 7 (ite (and ?v_13 (not (___z12z___ ?v_6))) 8 (ite (and ?v_14 (not (___z13z___ ?v_6))) 9 10))))))))))) (?v_16 (___z26z___ ?v_6)) (?v_1 (ite ?v_4 0 (ite ?v_5 1 (ite ?v_7 2 (ite ?v_8 3 (ite ?v_9 4 (ite ?v_10 5 (ite ?v_11 6 (ite ?v_12 7 (ite ?v_13 8 (ite ?v_14 9 10)))))))))))) (let ((?v_2 (ite ?v_3 0 (ite (<= ?v_1 9) ?v_1 0)))) (= (___z26z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) ?v_2 (ite (___z22z___ ?v_0) (ite (___z23z___ ?v_0) ?v_2 (ite ?v_3 0 (ite (<= ?v_15 9) ?v_15 ?v_16))) ?v_16))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z61z___ ?v_0))) (= (___z69z___ ?v_0) (ite (___z66z___ ?v_0) (ite (___z62z___ ?v_0) (ite (not (= (___z60z___ ?v_0) 3)) 3 ?v_1) ?v_1) (___z74z___ ?v_0))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z73z___ ?v_0))) (= (___z71z___ ?v_0) (ite (not (= ?v_1 4)) 4 ?v_1)))))
(assert (___z15z___ (+ _n (- 1))))
(assert (not (or (not (= _base (- 1))) (___z15z___ _n))))
(assert true)
(set-info :status unsat)
(check-sat)
(exit)
